/* Benchmarks for the PionterC verifier. */

// list visit


struct list
{
  int data;
  struct list* next;
};

/*@ let list(l) = (l==null) ||
  @                  (({l}) && list(l->next))
  @ in  list(l)
  @ end
  @*/

int traverse (struct list* l)
{
  int sum;
  struct list* p;
  sum = 0;
  p = l;
  if (l!=null)
  {
    while (p!=null) /*@ (forall i:int. forall j:int. (({l(->next)i, p} && {l(->next)j}) && i!=j))
                      @    || (forall i:int. exists j:int. (({l(->next)i}) && ({l(->next)j, p}N) && (i<j)))
                      @*/
   {
     sum = sum + p->data;
     p = p->next;
   }
    return sum;
  }
  else return 0;
}
/*@ list(l)
  @*/
  
